Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    x - 0  → x
2:    s(x) - s(y)  → x - y
3:    min(x,0)  → 0
4:    min(0,y)  → 0
5:    min(s(x),s(y))  → s(min(x,y))
6:    twice(0)  → 0
7:    twice(s(x))  → s(s(twice(x)))
8:    f(s(x),s(y))  → f(y - min(x,y),s(twice(min(x,y))))
9:    f(s(x),s(y))  → f(x - min(x,y),s(twice(min(x,y))))
There are 9 dependency pairs:
10:    s(x) -# s(y)  → x -# y
11:    MIN(s(x),s(y))  → MIN(x,y)
12:    TWICE(s(x))  → TWICE(x)
13:    F(s(x),s(y))  → F(y - min(x,y),s(twice(min(x,y))))
14:    F(s(x),s(y))  → y -# min(x,y)
15:    F(s(x),s(y))  → F(x - min(x,y),s(twice(min(x,y))))
16:    F(s(x),s(y))  → x -# min(x,y)
17:    F(s(x),s(y))  → TWICE(min(x,y))
18:    F(s(x),s(y))  → MIN(x,y)
The approximated dependency graph contains 4 SCCs: {10}, {11}, {12} and {13,15}.
Tyrolean Termination Tool  (0.27 seconds)   ---  May 4, 2006